package sve;

import java.util.ArrayList;
import java.util.Collection;
import java.util.HashMap;
import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Set;

import xadd.XADD;
import xadd.XADD.BoolDec;
import cmdp.HierarchicalParser;

public class Buffer {

	private ArrayList<String> _boolVars;
	private HashMap<String, XADD> _cases;
	private HashMap<String, Integer> _varIds;
	private HashMap<String, XADD> _delta;
	private HashMap<String, Integer> _deltaIds;

	public Set<String> getVars() {
		return _cases.keySet();
	}

	public HashMap<String, Integer> getVarIds() {
		return _varIds;
	}

	public ArrayList<String> getBoolVars() {
		return _boolVars;
	}

	public HashMap<String, XADD> getCases() {
		return _cases;
	}

	public HashMap<String, XADD> getDelta() {
		return _delta;
	}

	public boolean isBoolean(String var) {
		return _boolVars.contains(var);
	}

	public boolean checkIntegrity() {
		for (String var : _varIds.keySet()) {
			if (!isContainedInVars(var)) {
				exit("Unreferenced variable " + var + "! Check your input file");
				return false;
			}
		}

		return true;
	}

	private boolean isContainedInVars(String var) {
		for (String v : _cases.keySet()) {
			if (Utils.contains(var, _cases.get(v).collectVars(_varIds.get(v)))) {
				return true;
			}
		}
		return false;
	}

	public Buffer(ArrayList input) {
		_boolVars = new ArrayList<String>();
		_cases = new HashMap<String, XADD>();
		_varIds = new HashMap<String, Integer>();
		_delta = new HashMap<String, XADD>();
		_deltaIds = new HashMap<String, Integer>();

		if (input == null) {
			System.out.println("Empty input file!");
			System.exit(1);
		}

		// take care of booleans :D
		buildXADDs(input);
	}

	public static Buffer parse(String filepath) {
		return new Buffer(HierarchicalParser.ParseFile(filepath));
	}

	private void buildXADDs(ArrayList input) {
		HashMap<String, XADD> data = new HashMap<String, XADD>();

		if (input == null) {
			System.out.println("Empty input file!");
			System.exit(1);
		}

		Iterator i = input.iterator();
		Object o;

		// Set up variables

		o = i.next();
		if (!(o instanceof String) || !((String) o).equalsIgnoreCase("bvariables")) {
			exit("Missing bvariable declarations: " + o);
		}
		// TODO: Add all boolean vars to XADD

		o = i.next();
		_boolVars.addAll((Collection<? extends String>) o);
		// // TODO: Add all intermediate boolean vars to XADD

		// Set up cases
		while (i.hasNext()) {
			o = i.next();
			if (!(o instanceof String) || !((String) o).equalsIgnoreCase("case")) {
				break;
			}

			// o == "cases"
			String aname = (String) i.next();
			System.out.println("case: " + aname);
			// HashMap<String, ArrayList> cpt_map = new HashMap<String, ArrayList>();

			o = i.next();
			while (!((String) o).equalsIgnoreCase("endcase")) {// endaction
				String v = (String) o;
				o = i.next();
				XADD x = new XADD();
				if (o instanceof String && ((String) o).equalsIgnoreCase("delta")) {
					o = i.next();
					int xadd = x.buildCanonicalXADD(((ArrayList) o));
					_deltaIds.put(v, xadd);
					_delta.put(v, x);
					// Utils.print((List) o);
				} else {
					int xadd = x.buildCanonicalXADD(((ArrayList) o));
					_varIds.put(v, xadd);
					if (isBoolean(v)) {
						int idx = x.getVarIndex(x.new BoolDec(v), true);
						int high_branch = xadd;
						int low_branch = x.apply(x.getTermNode(XADD.ONE), high_branch, XADD.MINUS);
						xadd = x.getINode(idx, low_branch, high_branch);
						xadd = x.makeCanonical(xadd);
					}
					_cases.put(v, x);
				}
				o = i.next();
			}
		}

		checkIntegrity();
	}

	private static void exit(String s) {
		new Exception(s).printStackTrace();
		System.exit(-1);
	}

	public ArrayList<ArrayList<Integer>> getReferences(String var) {
		ArrayList<Integer> cases = new ArrayList<Integer>();
		ArrayList<Integer> deltas = new ArrayList<Integer>();
		for (String key : getVars()) {
			int id = getId(var);
			XADD x = getCase(var);
			if (x == null)
				continue;
			if (x.collectVars(id).contains(var)) {
				cases.add(id);
			}
			id = getDeltaId(var);
			x = getDelta(var);
			if (x == null)
				continue;
			if (x != null && x.collectVars(id).contains(var)) {
				deltas.add(id);
			}
		}

		ArrayList<ArrayList<Integer>> a = new ArrayList<ArrayList<Integer>>();
		a.add(cases);
		a.add(deltas);

		return a;
	}

	public int getId(String var) {
		return _varIds.get(var);
	}

	public ArrayList<ArrayList<Integer>> getIds(String[] qu) {
		ArrayList<ArrayList<Integer>> ids = new ArrayList<ArrayList<Integer>>();
		ids.add(new ArrayList<Integer>());
		ids.add(new ArrayList<Integer>());

		for (String var : qu) {
			ids.get(0).add(getId(var));
			int d = getDeltaId(var);
			if (d >= 0)
				ids.get(1).add(d);
		}

		return ids;
	}

	public int getDeltaId(String var) {
		if (!_deltaIds.containsKey(var)) {
			return -1;
		}
		return _deltaIds.get(var);
	}

	public XADD getCase(String var) {
		return _cases.get(var);
	}

	public XADD getCase(int id) {
		for (String s : _cases.keySet()) {
			if (getId(s) == id) {
				return getCase(s);
			}
		}
		return null;
	}

	public XADD getDelta(String var) {
		return _delta.get(var);
	}

	public ArrayList<ArrayList<Integer>> getReferences(String[] q) {
		ArrayList<ArrayList<Integer>> all = new ArrayList<ArrayList<Integer>>();
		all.add(new ArrayList<Integer>());
		all.add(new ArrayList<Integer>());
		for (String qq : q) {
			ArrayList<ArrayList<Integer>> a = getReferences(qq);
			all.get(0).addAll(a.get(0));
			all.get(1).addAll(a.get(1));
		}

		return all;
	}
}
